feat(Stir): prove out_of_dom_smpl_1 (out-of-domain sampling bound, 1 sorry removed) - #638

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Prove STIR out-of-domain sampling bound

sorry delta: -1 (1 removed) — net proof progress

Proof Completion (sorries removed)

• out_of_dom_smpl_1 (in ArkLib/ProofSystem/Stir/OutOfDomSmpl.lean): The sorry placeholder has been replaced with a full proof. The proof uses three new private lemmas: prob_exists_le_sum (union bound for probabilities), prob_uniform_fin_forall (probability that a random function from Fin s satisfies a pointwise condition), and card_eval_eq_le (bounds count of evaluation collisions by degree-1). A cast helper coe_choose_two_nnreal is also added. No new sorry or admit are introduced anywhere.

Mathematical Formalization

• outOfDomainSamplingBound: A new public top-level proposition formalizing the polymorphic form of Lemma 4.5.2 (STIR out-of-domain sampling bound).
• out_of_dom_smpl_2_statement: A new public lemma that proves outOfDomainSamplingBound by rewriting the pre-existing out_of_dom_smpl_2. This serves as a compact consumer-facing interface whose kernel dependency closure reaches the full theorem.
• The existing definitions listDecodingCollisionProbability and the lemma out_of_dom_smpl_2 remain unchanged.

Refactoring / API Changes

• Combine.block_size (in ArkLib/ProofSystem/Stir/Combine.lean): Changed from private to public, and a docstring added explaining its use in the type of master_lemma and by downstream consumers that need to reference it without relying on a private generated name.

Infrastructure / CI

• set_option maxHeartbeats increases in OutOfDomSmpl.lean: two increases (1,000,000 and 5,000,000) are applied to the new top-level definitions (outOfDomainSamplingBound and out_of_dom_smpl_2_statement) to accommodate the elaboration budget. No other infrastructure or CI changes.

Scope and Context

The core mathematical change is the proof completion and new formalization in OutOfDomSmpl.lean; the Combine.lean change is a minor visibility adjustment. The PR does not claim end-to-end STIR soundness or full correspondence with informal paper claims, only that the selected ArkLib proposition is now proven under its current definitions and allowed Lean axioms.

Statistics

Lean Declarations

sorry Tracking

Last updated: 2026-07-12 18:54 UTC.

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

Mathematical Formalization

• Completed proof of out_of_dom_smpl_1 (Lemma 4.5.1) in OutOfDomSmpl.lean, which was previously blocked by a sorry. This is the core contribution.
• Added four private helper lemmas used in the above proof:
  • prob_exists_le_sum
  • prob_uniform_fin_forall
  • card_eval_eq_le
  • coe_choose_two_nnreal
• Introduced a compact consumer proposition outOfDomainSamplingBound that packages the statement of out_of_dom_smpl_2 (Lemma 4.5.2). The lemma out_of_dom_smpl_2_statement proves it by unfolding the definition, providing a kernel-verifiable bridge for downstream tools with bounded heartbeat requirements.
• Visibility change in Combine.lean: the definition block_size was made public (previously private) with a doc comment explaining that it must be accessible because it appears in the type of master_lemma. Downstream consumers now refer to it without relying on a generated private name.

Proof Completion (sorries removed)

• 1 sorry removed: the proof of out_of_dom_smpl_1 is now fully filled in. All other statements (listDecodingCollisionProbability, the type of out_of_dom_smpl_2) remain unchanged.
• No new sorry or admit placeholders appear in any changed file.

Infrastructure / CI

• Increased maxHeartbeats for the out_of_dom_smpl_1 proof in OutOfDomSmpl.lean to accommodate the computational weight of the completed proof.

Documentation

• Added doc comment on block_size in Combine.lean justifying why it is exposed and clarifying its role in master_lemma’s type.

Summary of scope

• The entire change is concentrated in two files: Combine.lean (single visibility + doc change) and OutOfDomSmpl.lean (the main proof fulfillment, new lemmas, and the compact proposition). The proofs rely only on allowed Lean axioms (propext, Classical.choice, Quot.sound).

Statistics

Lean Declarations

sorry Tracking

Last updated: 2026-08-02 22:16 UTC.